Problem:
 U11(tt(),M,N) -> U12(tt(),M,N)
 U12(tt(),M,N) -> s(plus(N,M))
 plus(N,0()) -> N
 plus(N,s(M)) -> U11(tt(),M,N)

Proof:
 Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {6,5,4}
   transitions:
    U111(7,2,1) -> 16,14,10,6
    U111(7,1,3) -> 16,14,10,6
    U111(7,3,3) -> 16,14,10,6
    U111(7,2,2) -> 16,14,10,6
    U111(7,1,1) -> 16,14,10,6
    U111(7,3,1) -> 16,14,10,6
    U111(7,2,3) -> 16,14,10,6
    U111(7,1,2) -> 16,14,10,6
    U111(7,3,2) -> 16,14,10,6
    tt1() -> 7*
    s1(10) -> 5*
    plus1(3,1) -> 10*
    plus1(3,3) -> 10*
    plus1(1,2) -> 10*
    plus1(2,1) -> 10*
    plus1(2,3) -> 10*
    plus1(3,2) -> 10*
    plus1(1,1) -> 10*
    plus1(1,3) -> 10*
    plus1(2,2) -> 10*
    U121(7,2,1) -> 4*
    U121(7,1,3) -> 4*
    U121(7,3,3) -> 4*
    U121(7,2,2) -> 4*
    U121(7,1,1) -> 4*
    U121(7,3,1) -> 4*
    U121(7,2,3) -> 4*
    U121(7,1,2) -> 4*
    U121(7,3,2) -> 4*
    s2(14) -> 4*
    plus2(3,1) -> 14*
    plus2(3,3) -> 14*
    plus2(1,2) -> 14*
    plus2(2,1) -> 14*
    plus2(2,3) -> 14*
    plus2(3,2) -> 14*
    plus2(1,1) -> 14*
    plus2(1,3) -> 14*
    plus2(2,2) -> 14*
    U110(1,1,1) -> 4*
    U110(1,3,1) -> 4*
    U110(1,2,3) -> 4*
    U110(2,2,1) -> 4*
    U110(2,1,3) -> 4*
    U110(2,3,3) -> 4*
    U110(3,1,1) -> 4*
    U110(1,1,2) -> 4*
    U110(3,3,1) -> 4*
    U110(1,3,2) -> 4*
    U110(3,2,3) -> 4*
    U110(2,2,2) -> 4*
    U110(3,1,2) -> 4*
    U110(3,3,2) -> 4*
    U110(1,2,1) -> 4*
    U110(1,1,3) -> 4*
    U110(1,3,3) -> 4*
    U110(2,1,1) -> 4*
    U110(2,3,1) -> 4*
    U110(2,2,3) -> 4*
    U110(3,2,1) -> 4*
    U110(1,2,2) -> 4*
    U110(3,1,3) -> 4*
    U110(3,3,3) -> 4*
    U110(2,1,2) -> 4*
    U110(2,3,2) -> 4*
    U110(3,2,2) -> 4*
    U122(11,1,1) -> 16,14,10,6
    U122(11,3,1) -> 16,14,10,6
    U122(11,2,3) -> 16,14,10,6
    U122(11,1,2) -> 16,14,10,6
    U122(11,3,2) -> 16,14,10,6
    U122(11,2,1) -> 16,14,10,6
    U122(11,1,3) -> 16,14,10,6
    U122(11,3,3) -> 16,14,10,6
    U122(11,2,2) -> 16,14,10,6
    tt0() -> 1*
    tt2() -> 11*
    U120(1,1,1) -> 5*
    U120(1,3,1) -> 5*
    U120(1,2,3) -> 5*
    U120(2,2,1) -> 5*
    U120(2,1,3) -> 5*
    U120(2,3,3) -> 5*
    U120(3,1,1) -> 5*
    U120(1,1,2) -> 5*
    U120(3,3,1) -> 5*
    U120(1,3,2) -> 5*
    U120(3,2,3) -> 5*
    U120(2,2,2) -> 5*
    U120(3,1,2) -> 5*
    U120(3,3,2) -> 5*
    U120(1,2,1) -> 5*
    U120(1,1,3) -> 5*
    U120(1,3,3) -> 5*
    U120(2,1,1) -> 5*
    U120(2,3,1) -> 5*
    U120(2,2,3) -> 5*
    U120(3,2,1) -> 5*
    U120(1,2,2) -> 5*
    U120(3,1,3) -> 5*
    U120(3,3,3) -> 5*
    U120(2,1,2) -> 5*
    U120(2,3,2) -> 5*
    U120(3,2,2) -> 5*
    s3(16) -> 16,14,10,6
    s0(2) -> 2*
    s0(1) -> 2*
    s0(3) -> 2*
    plus3(3,1) -> 16*
    plus3(3,3) -> 16*
    plus3(1,2) -> 16*
    plus3(2,1) -> 16*
    plus3(2,3) -> 16*
    plus3(3,2) -> 16*
    plus3(1,1) -> 16*
    plus3(1,3) -> 16*
    plus3(2,2) -> 16*
    plus0(3,1) -> 6*
    plus0(3,3) -> 6*
    plus0(1,2) -> 6*
    plus0(2,1) -> 6*
    plus0(2,3) -> 6*
    plus0(3,2) -> 6*
    plus0(1,1) -> 6*
    plus0(1,3) -> 6*
    plus0(2,2) -> 6*
    00() -> 3*
    1 -> 16,14,10,6
    2 -> 16,14,10,6
    3 -> 16,14,10,6
  problem:
   
  Qed